package model;

import edu.uci.ics.jung.graph.DelegateTree;
import edu.uci.ics.jung.io.GraphMLWriter;
import java.io.BufferedWriter;
import java.io.FileWriter;
import java.io.IOException;
import java.io.PrintWriter;
import java.util.Collection;
import java.util.Date;
import java.util.LinkedList;
import model.exceptions.FormulaException;
import model.exceptions.OperatorException;

public class Prover {

    private int edgeCounter;
    private DelegateTree<Formula, Integer> tree;
    private LinkedList<Formula> leaves, finalLeaves, errorFormulas, errorLeaves;
    /**
     * czy dowód nie wprost <br/> 1 - dowód nie wprost - porządany stan formuły:
     * false (domknięcie)- wszystkie gałęzie <br/> -1 - klasyczny dowód -
     * porządany stan formuły: true (otwarcie)- conajmniej 1 gałąź <br/> mnożnik
     * *2 - rozwijać do końca drzewo literałów w przypadku stwierdzenia
     * porządanego efektu
     */
    private int reductioAdAbsurdum;

    /**
     *
     * @param _orgFormula zdefiniowana formula
     * @param _priorities operatory ułożone według priorytetu, pierwsza MUSI być
     * negacja
     * @param negate 1 - negować formułę <br/> -1 - zostawić orginalną formułę
     * <br/> mnożnik *2 - rozwijać do końca drzewo literałów
     * @throws Exception
     */
    public Prover(String _orgFormula, LinkedList<Operator> _priorities, int _reductioAdAbsurdum)
            throws FormulaException, Exception {
        this.tree = new DelegateTree<Formula, Integer>();
        this.finalLeaves = new LinkedList<Formula>();
        this.errorFormulas = new LinkedList<Formula>();
        this.errorLeaves = new LinkedList<Formula>();
        this.leaves = new LinkedList<Formula>();
        this.edgeCounter = 0;
        this.reductioAdAbsurdum = _reductioAdAbsurdum;

        String formula = _orgFormula.replaceAll("\\s", "");

        this.tree.setRoot(new Formula(formula, 0 < this.reductioAdAbsurdum, _priorities));
        this.leaves.add(this.tree.getRoot());

        Formula form = this.tree.getRoot();

        //walidacja formuły
        Formula.validate(form.getFormulaToDo(), form.getPriorities());
    }

    public boolean isClassicProof() {
        return this.reductioAdAbsurdum < 0;
    }

    /**
     * pomocniczna metoda do wypisania aktualnego czasu i pamięci zajmowanej
     * przez program
     *
     * @return napis z info
     */
    private String printDateAndMemory() {
        //System.out.println(Runtime.getRuntime().totalMemory());
        //System.out.println(Runtime.getRuntime().maxMemory());
        //System.out.println(Runtime.getRuntime().freeMemory());
        //long memMB = (Runtime.getRuntime().maxMemory() - Runtime.getRuntime().freeMemory()) / 1000000;
        return " - " + new Date(); //+ " - " + memMB + "MB";
    }

    /**
     * sprawdza poprawność formuły wybranym dowodem
     *
     * @return czy drzewo jest otwarte
     * @throws Exception
     */
    public boolean prove() throws OperatorException, FormulaException, ArrayIndexOutOfBoundsException {
        //System.out.println("Prover.prove()" + this.printDateAndMemory());

        while (!this.leaves.isEmpty()) {
            Formula current = this.leaves.poll();
            Collection<Formula> newFormulas = current.makeChildren();
            for (Formula leaf : newFormulas) {
                this.leaves.push(leaf);
                this.tree.addChild(++this.edgeCounter, current, leaf);
                leaf.setForumlaNumber(this.edgeCounter);


                if (this.edgeCounter % 10000 == 0) {
                    System.out.println("node count: " + leaf.getFormulaNumber() + this.printDateAndMemory());

                    //obliczanie ile jeszcze conajmniej węzłów jest do przemielenia
                    /*if (this.edgeCounter % 1000000 == 0) {
                     int cnt = 0;
                     for(Formula ll : this.leaves){
                     cnt += ll.getTodoSize();
                     }
                     System.out.println("It is known "+cnt+" nodes waiting to created. And they are about to have some new childrem-nodes.");
                     }*/
                }

                if (current.getCorrectness()) {
                    // liść nie zgadza się ze sposobem dowodzenia:
                    // klasyczny == false, nie wprost == true
                    this.errorFormulas.add(leaf);
                }
            }

            if (newFormulas.isEmpty() && current.getTodoSize() == 0) {
                this.finalLeaves.add(current);
                if (current.getCorrectness()) {
                    // jedna galaz nie zgadza sie ze stanem porządanym w sposobie dowdzenia:
                    // klasyczny == false, nie wprost == true
                    this.errorLeaves.add(current);
                }

                if ((this.reductioAdAbsurdum == 1 || this.reductioAdAbsurdum == -1)
                        && current.getCorrectness()) {
                    // opcja wcześniejszego kończenia  dowodu + OTWARTA gałąź
                    // dla klasycznego dowodu - poprawny liść - dowiedzono poprawnośći
                    // dla nie wprost - poprawny liść - nie można udowodnić poprawności (prawdopodnie jest false)

                    return this.getState();
                }
            }
        }

        return this.getState();
    }

    /**
     * czy wprowadzona formuła jest prawdziwa
     *
     * @return czy drzewo jest otwarte
     */
    public boolean getState() throws FormulaException {
        if (this.finalLeaves == null || this.finalLeaves.isEmpty()) {
            throw new FormulaException("proving hasn't started");
        }

        //System.out.println("Prover.getState()" + this.printDateAndMemory());
        //this.printTree();

        for (Formula form : this.finalLeaves) {
            if (form.getCorrectness()) {
                // poprawny liść - OTWARTA GAŁĄŹ
                return true;
            }
        }

        // wszystkie liście niepoprawne - wszystkie gałęzie domknięte
        return false;
    }
    
    /**
     * interpretacja otwartości drzewa względem wybranego dowodu
     * @returns czy formuła jest prawdziwa
     */
    public boolean isFormulaTrue(){
        if(this.getState()){
            // poprawny liść - OTWARTA GAŁĄŹ
            // dla klasycznego dowodu - poprawny liść - dowiedzono poprawnośći
            // dla nie wprost - poprawny liść - nie można udowodnić poprawności org formuły (prawdopodnie jest false)

            //System.out.println("Prover.getState(): dowód:" + this.reductioAdAbsurdum + ", znaleziono OTWARTĄ gałąź");

            // dla klasycznego dowodu - true
            // dla nie wprost - false
            return this.isClassicProof();
        }
        
        // wszystkie liście niepoprawne - wszystkie gałęzie domknięte
        // dla klasycznego dowodu - nie dowiedzono poprawności => fałszywe
        // dla nie wprost - dowiedzono fałszywości zaprzeczenia => prawdzia org formuła

        //System.out.println("Prover.getState(): dowód:" + this.reductioAdAbsurdum + ", znaleziono DOMKNIĘTĄ gałąź");

        // dla klasycznego dowodu - false
        // dla nie wprost - true
        return !this.isClassicProof();
    }

    /**
     * wypisuje całe drzewo, wylistowywuje dzieci dodatkowo
     */
    public String printTree() {
        String ret = "CREATED TREE: \n" + "all nodes: \n";
        ret = ret + Prover.printTree(this.tree);
        int fsize = this.finalLeaves.size();
        ret = ret + "final leaves (size= " + fsize + "):\n";
        ret = ret + Prover.printLeaves(this.finalLeaves) + "\n";
        fsize = this.errorFormulas.size();
        if (fsize > 0) {
            ret = ret + "error formulas (size= " + fsize + "):\n";
            ret = ret + Prover.printLeaves(this.errorFormulas) + "\n";
        }
        fsize = this.errorLeaves.size();
        if (fsize > 0) {
            ret = ret + "error leaves (size= " + fsize + "):\n";
            ret = ret + Prover.printLeaves(this.errorLeaves);
        }

        return ret;
    }

    /**
     * wypisuje dostarczone drzewo
     *
     * @param tree
     */
    public static String printTree(DelegateTree<Formula, Integer> tree) {
        String ret = Prover.printTreeChildren(tree, tree.getRoot(), 1);
        return ret;
        //   System.out.println("Prover.tree.getVertexCount(): " + tree.getVertexCount());
    }

    /**
     * wypisuje wszystkie liście z listy
     *
     * @param leaves
     */
    public static String printLeaves(LinkedList<Formula> leaves) {
        String r = "";
        for (Formula form : leaves) {
            r = r + "correctness: " + form.getCorrectness() + ", " + form + "\n";
        }
        return r;
    }

    /**
     * wypisuje pokolenie dzieci
     *
     * @param parent rodzic dla którego wypisujemy dzieci
     * @param lvl - numer porządkowy dla wypisywania
     */
    protected static String printTreeChildren(DelegateTree<Formula, Integer> tree, Formula parent, int lvl) {
        String text = "";
        String newt, newt2;
        for (Formula child : tree.getChildren(parent)) {
            newt = "child " + lvl + ": childrenCnt: " + tree.getChildCount(child)
                    + ", parentEdge: " + tree.getParentEdge(child) + "\n       parent: "
                    + tree.getParent(child) + "\n       me: " + child;
            text = text + newt + "\n";
            newt2 = Prover.printTreeChildren(tree, child, lvl + 1);
            text = text + newt2;
        }
        text = text + "\n";
        return text;
    }

    /**
     * zwraca wszystkie wierzchołki drzewa które są zgodne ze stanem porządanym
     * przy sposobie dowodzenia<br/> klasyczny != true, nie wprost != false
     * <br/> stosować przy: dowodzeniu do napotkania sprzeczności
     *
     * @return
     */
    public LinkedList<Formula> getErrorFormulas() {
        return this.errorFormulas;
    }

    /**
     * zwraca wszystkie liście drzewa które są zgodne ze stanem porządanym przy
     * sposobie dowodzenia<br/> klasyczny != true, nie wprost != false <br/>
     * stosować przy: dowodzeniu z pełnym rozwinięciem drzewa
     *
     * @return
     */
    public LinkedList<Formula> getErrorLeaves() {
        return this.errorLeaves;
    }

    /**
     * zwraca drzewo formuł
     */
    public DelegateTree<Formula, Integer> getTree() {
        return this.tree;
    }

    /**
     * zapisuje graf do pliku o podanej ścieżce
     *
     * @param path ścieżka do pliku
     * @throws IOException
     */
    public void saveTree(String path) throws IOException {
        GraphMLWriter<Formula, Integer> graphWriter = new GraphMLWriter<Formula, Integer>();
        PrintWriter out = new PrintWriter(new BufferedWriter(new FileWriter(path)));
        graphWriter.save(this.tree, out);
    }
}
